# FormalRV.Arithmetic Logical arithmetic gadgets (Cuccaro/Gidney adders, modular multiplier, unary lookup) and their semantic-correctness proofs. This umbrella imports every module under `Arithmetic/`.

(no documented top-level declarations)

FormalRV.Audit — one reader-facing audit file per paper. Each `FormalRV/Audit/<Paper>/` holds ONLY that paper's specific implementation + scheduling, and imports ONLY general/reusable code from the framework folders (`Shor`, `LatticeSurgery`, `QEC`, `System`, `PPM`, `Framework`, `Verifier`, …) — never another paper. Its layer files expose the relevant theorems with `#check` / `#verify_clean`, framed by a docstring that states the paper's headline claim, the SETTINGS a reader should check against the paper, OUR APPROACH, the GAP we determined, and what is STILL UNSOLVED. A reader verifies any single paper with, e.g., lake build FormalRV.Audit.Gidney2025 Compilation confirms every cited theorem type-checks; the `#print axioms` lines reveal the exact trust base. See FormalRV/Audit/README.md for the index table.

(no documented top-level declarations)

# FormalRV.Codegen Code-emission (the `DEVICE-PROGRAM` / QASM serializers). This umbrella imports the *library* codegen modules that are part of the umbrella `lake build`. The `#eval`-driven demo modules (`SysCallEmitDemo.lean`, `WindowedEmitDemo.lean`, the QASM demos) are intentionally NOT imported here — they print on elaboration and are run on demand with `lake env lean <file>`.

(no documented top-level declarations)

# FormalRV.Core Definitions: the Gate IR, classical & quantum (matrix) semantics, gate decompositions. This umbrella imports every module under `Core/`.

(no documented top-level declarations)

# FormalRV.Framework The four inter-layer contract interfaces (L1 algorithm, L2 gadgets, L3 PPM, L4 QEC code) + error mechanisms. This umbrella imports every module under `Framework/`.

(no documented top-level declarations)

# FormalRV.LatticeSurgery Lattice-surgery merge/split modelling and its PPM/system-call contracts. This umbrella imports every module under `LatticeSurgery/`.

(no documented top-level declarations)

# FormalRV.PPM Pauli-product measurement: Pauli algebra, the Gottesman update, circuit-to-PPM compilation, magic-state factories. This umbrella imports every module under `PPM/`.

(no documented top-level declarations)

# FormalRV.QEC Quantum error-correcting code definitions (qLDPC parity matrices, code instances). This umbrella imports every module under `QEC/`.

(no documented top-level declarations)

# FormalRV.Qualtran Data bridge mirroring Qualtran's PhysicalParameters into Lean. This umbrella imports every module under `Qualtran/`.

(no documented top-level declarations)

# FormalRV.Shor The main result: Shor order-finding success probability (see `Shor/Main.lean`), QPE, phase kickback, inverse-QFT. This umbrella imports every module under `Shor/`.

(no documented top-level declarations)

================================================================================ FormalRV.StandardShor — START HERE if you are new to this system. ================================================================================ This is the **standard, textbook implementation of Shor's algorithm + surface-code lattice surgery** — the teaching baseline. It is the version to read first, *before* the advanced low-overhead tricks (qLDPC / lifted-product / generalised-bicycle codes, windowed Ekerå–Håstad, factory sharing, …) that the corpus papers layer on top. It REDEFINES NOTHING. It curates and RE-EXPORTS, under the single namespace `FormalRV.StandardShor`, the verified results that make up the standard pipeline, so a newcomer has one clean place to find them. (The underlying proofs of the order-finding success bound are PORTED FROM the Coq `SQIR` project — that attribution is preserved in the original `FormalRV.SQIRPort.*` names, which these are aliases of.) LEARNING PATH — the four steps of "standard Shor on a surface code": 1. THE ALGORITHM SUCCEEDS. Order finding succeeds with probability ≥ κ/(log₂N)⁴ (κ = 4·e⁻²/π²), N-parametric, for any correct modular-multiplier oracle. 2. THE CIRCUIT IS CORRECT. A concrete SQIR-faithful modular multiplier (built from the verified Cuccaro adder) implements that oracle. 3. THE LOGICAL GATES ARE LATTICE SURGERY. On the distance-3 surface code, a logical CNOT is a verified ZZ-merge + XX-merge, and a Toffoli is a verified |C̄CZ̄⟩ injection. 4. END TO END. The Shor PPM program is physically realized as a surface-code surgery schedule that reduces the stabilizer state and satisfies the system invariants. A reader can verify the whole baseline with: `lake build FormalRV.StandardShor`. See FormalRV/StandardShor/README.md for the narrative guide.

(no documented top-level declarations)

# FormalRV.System System invariants: scheduling, layout, architecture, capacity/latency/bandwidth checks. This umbrella imports every module under `System/`. *Single entry point:** `FormalRV.System.FTFramework` is the coherent front door tying the two scheduling subsystems together — canonical hardware (`HardwareParams.MachineParams`, one decoder- reaction budget), schedule well-formedness (`DeviceSchedule.scheduleValid` / `ScheduleInv.all_invariants_ok`), the resource BRACKET (`ScheduleBounds.resource_bracket`: lower floor ≤ workload ≤ upper ceiling, with `naive_peak_le_total` the peak ≤ footprint upper bound), and hardware SENSITIVITY (`HardwareSensitivity.HW.timeLB`). The two naive efforts (`NaiveSchedule` over `DSchedule`, `NaiveUpperBound` over `ResourceEstimate`) and the two checkers (`DeviceSchedule` over `DeviceOp`, `InvariantFramework` over `SysCall`) are connected by theorems, not merged.

(no documented top-level declarations)

# FormalRV.Verifier The verifier: an airtight, user-fixed specification of a correct Shor implementation on a user-supplied LP code, plus the `#verify_clean` enforcement gate that REJECTS any submission which is incomplete (`sorry`) or leans on an extra axiom. Set the spec first; build the construction second; the gate decides acceptance.

(no documented top-level declarations)